Theorem pm4.71rd 554

Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)

Hypothesis

Ref	Expression
pm4.71rd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
pm4.71rd	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Proof of Theorem pm4.71rd

Step	Hyp	Ref	Expression
1		pm4.71rd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		pm4.71r 550	. 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜒 ∧ 𝜓)))
3	1, 2	sylib 209	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  reueubd  3360  2reu5  3621  ralss  3872  rexss  3873  reuhypd  5099  exopxfr2  5475  dfco2a  5856  feu  6298  funbrfv2b  6464  dffn5  6465  feqmptdf  6475  eqfnfv2  6537  dff4  6598  fmptco  6622  dff13  6739  opiota  7464  mpt2xopovel  7584  brtpos  7599  dftpos3  7608  erinxp  8059  qliftfun  8070  pw2f1olem  8306  infm3  11270  prime  11727  predfz  12691  hashf1lem2  13460  hashle2prv  13480  oddnn02np1  15295  oddge22np1  15296  evennn02n  15297  evennn2n  15298  smueqlem  15434  vdwmc2  15903  acsfiel  16522  subsubc  16720  ismgmid  17472  eqger  17849  eqgid  17851  gaorber  17945  symgfix2  18040  psrbaglefi  19584  znleval  20113  bastop2  21016  elcls2  21096  maxlp  21169  restopn2  21199  restdis  21200  1stccn  21484  tx1cn  21630  tx2cn  21631  imasnopn  21711  imasncld  21712  imasncls  21713  idqtop  21727  tgqtop  21733  filuni  21906  uffix2  21945  cnflf  22023  isfcls  22030  fclsopn  22035  cnfcf  22063  ptcmplem2  22074  xmeter  22455  imasf1oxms  22511  prdsbl  22513  caucfil  23298  cfilucfil4  23335  shft2rab  23495  sca2rab  23499  mbfinf  23652  i1f1lem  23676  i1fres  23692  itg1climres  23701  mbfi1fseqlem4  23705  iblpos  23779  itgposval  23782  cnplimc  23871  ply1remlem  24142  plyremlem  24279  dvdsflsumcom  25134  fsumvma2  25159  vmasum  25161  logfac2  25162  chpchtsum  25164  logfaclbnd  25167  lgsquadlem1  25325  lgsquadlem2  25326  lgsquadlem3  25327  dchrisum0lem1  25425  colinearalg  26010  nbgrelOLD  26456  nbusgreledg  26471  nbusgredgeu0  26492  umgr2v2enb1  26656  iswwlksnx  26967  wspniunwspnon  27069  clwlknf1oclwwlknlem2  27252  clwlknf1oclwwlkn  27254  eupth2lem2  27398  eupth2lems  27417  frgrncvvdeqlem2  27481  fusgr2wsp2nb  27515  fusgreg2wsp  27517  pjpreeq  28591  elnlfn  29121  fimarab  29778  fmptcof2  29790  dfcnv2  29809  2ndpreima  29818  f1od2  29832  fpwrelmap  29841  iocinioc2  29874  nndiffz1  29881  indpi1  30413  1stmbfm  30653  2ndmbfm  30654  eulerpartlemgh  30771  bnj1171  31396  mrsubrn  31738  elfuns  32348  fneval  32673  topdifinfindis  33512  uncf  33703  phpreu  33708  poimirlem23  33747  poimirlem26  33750  poimirlem27  33751  areacirclem5  33818  prter3  34663  islshpat  34799  lfl1dim  34903  glbconxN  35160  cdlemefrs29bpre0  36178  dib1dim  36947  dib1dim2  36950  diclspsn  36976  dihopelvalcpre  37030  dih1dimatlem  37111  mapdordlem1a  37416  hdmapoc  37713  rmydioph  38083  pw2f1ocnv  38106  rfovcnvf1od  38799  ntrneineine0lem  38882  funbrafv2b  41749  dfafn5a  41750