Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.21nii Structured version   Visualization version   GIF version

Theorem pm5.21nii 367
 Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.)
Hypotheses
Ref Expression
pm5.21ni.1 (𝜑𝜓)
pm5.21ni.2 (𝜒𝜓)
pm5.21nii.3 (𝜓 → (𝜑𝜒))
Assertion
Ref Expression
pm5.21nii (𝜑𝜒)

Proof of Theorem pm5.21nii
StepHypRef Expression
1 pm5.21nii.3 . 2 (𝜓 → (𝜑𝜒))
2 pm5.21ni.1 . . 3 (𝜑𝜓)
3 pm5.21ni.2 . . 3 (𝜒𝜓)
42, 3pm5.21ni 366 . 2 𝜓 → (𝜑𝜒))
51, 4pm2.61i 176 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197 This theorem is referenced by:  elrabf  3392  sbcco  3491  sbc5  3493  sbcan  3511  sbcor  3512  sbcal  3518  sbcex2  3519  sbcel1v  3528  sbcreu  3548  eldif  3617  elun  3786  elin  3829  sbccsb2  4038  elpr2  4232  eluni  4471  eliun  4556  sbcbr123  4739  elopab  5012  opelopabsb  5014  opeliunxp2  5293  inisegn0  5532  brfvopabrbr  6318  elpwun  7019  elxp5  7153  opeliunxp2f  7381  tpostpos  7417  ecdmn0  7832  brecop2  7884  elixpsn  7989  bren  8006  elharval  8509  sdom2en01  9162  isfin1-2  9245  wdomac  9387  elwina  9546  elina  9547  lterpq  9830  ltrnq  9839  elnp  9847  elnpi  9848  ltresr  9999  eluz2  11731  dfle2  12018  dflt2  12019  rexanuz2  14133  even2n  15113  isstruct2  15914  xpsfrnel2  16272  ismre  16297  isacs  16359  brssc  16521  isfunc  16571  oduclatb  17191  isipodrs  17208  issubg  17641  isnsg  17670  oppgsubm  17838  oppgsubg  17839  isslw  18069  efgrelexlema  18208  dvdsr  18692  isunit  18703  isirred  18745  issubrg  18828  opprsubrg  18849  islss  18983  islbs4  20219  istopon  20765  basdif0  20805  dis2ndc  21311  elmptrab  21678  isusp  22112  ismet2  22185  isphtpc  22840  elpi1  22891  iscmet  23128  bcthlem1  23167  wlkcpr  26580  frgrusgrfrcond  27239  isvcOLD  27562  isnv  27595  hlimi  28173  h1de2ci  28543  elunop  28859  ispcmp  30052  elmpps  31596  eldm3  31777  opelco3  31802  elima4  31803  elno  31924  brsset  32121  brbigcup  32130  elfix2  32136  elsingles  32150  imageval  32162  funpartlem  32174  elaltxp  32207  ellines  32384  isfne4  32460  istotbnd  33698  isbnd  33709  isdrngo1  33885  isnacs  37584  sbccomieg  37674  elmnc  38023  2reu4  41511
 Copyright terms: Public domain W3C validator