Theorem pm4.71rd 555

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 551	. 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜒 ∧ 𝜓)))
3	1, 2	sylib 210	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  reueubd  3369  2reu5  3651  ralss  3920  rexss  3921  reuhypd  5172  exopxfr2  5561  dfco2a  5935  feu  6380  fcnvres  6382  funbrfv2b  6550  dffn5  6551  feqmptdf  6562  eqfnfv2  6626  dff4  6688  fmptco  6712  dff13  6836  opiota  7563  mpoxopovel  7687  brtpos  7702  dftpos3  7711  erinxp  8169  qliftfun  8180  pw2f1olem  8415  infm3  11399  prime  11874  predfz  12846  hashf1lem2  13625  hashle2prv  13645  oddnn02np1  15555  oddge22np1  15556  evennn02n  15557  evennn2n  15558  smueqlem  15697  vdwmc2  16169  acsfiel  16795  subsubc  16993  ismgmid  17744  eqger  18125  eqgid  18127  gaorber  18221  symgfix2  18317  psrbaglefi  19878  znleval  20418  bastop2  21321  elcls2  21401  maxlp  21474  restopn2  21504  restdis  21505  1stccn  21790  tx1cn  21936  tx2cn  21937  imasnopn  22017  imasncld  22018  imasncls  22019  idqtop  22033  tgqtop  22039  filuni  22212  uffix2  22251  cnflf  22329  isfcls  22336  fclsopn  22341  cnfcf  22369  ptcmplem2  22380  xmeter  22761  imasf1oxms  22817  prdsbl  22819  caucfil  23604  cfilucfil4  23642  shft2rab  23827  sca2rab  23831  mbfinf  23984  i1f1lem  24008  i1fres  24024  itg1climres  24033  mbfi1fseqlem4  24037  iblpos  24111  itgposval  24114  cnplimc  24203  ply1remlem  24474  plyremlem  24611  dvdsflsumcom  25482  fsumvma2  25507  vmasum  25509  logfac2  25510  chpchtsum  25512  logfaclbnd  25515  lgsquadlem1  25673  lgsquadlem2  25674  lgsquadlem3  25675  dchrisum0lem1  25809  colinearalg  26414  nbusgreledg  26853  nbusgredgeu0  26868  umgr2v2enb1  27026  iswwlksnx  27341  wspniunwspnon  27444  clwlknf1oclwwlknlem2  27622  clwlknf1oclwwlkn  27624  clwlknf1oclwwlknOLD  27626  eupth2lem2  27764  eupth2lems  27783  frgrncvvdeqlem2  27849  fusgr2wsp2nb  27883  fusgreg2wsp  27885  pjpreeq  28971  elnlfn  29501  fimarab  30169  fmptcof2  30181  dfcnv2  30201  2ndpreima  30219  f1od2  30233  fpwrelmap  30245  iocinioc2  30278  nndiffz1  30285  indpi1  30955  1stmbfm  31195  2ndmbfm  31196  eulerpartlemgh  31313  bnj1171  31949  mrsubrn  32317  elfuns  32934  fneval  33258  topdifinfindis  34106  uncf  34349  phpreu  34354  poimirlem23  34393  poimirlem26  34396  poimirlem27  34397  areacirclem5  34464  erim2  35393  prter3  35500  islshpat  35635  lfl1dim  35739  glbconxN  35996  cdlemefrs29bpre0  37014  dib1dim  37783  dib1dim2  37786  diclspsn  37812  dihopelvalcpre  37866  dih1dimatlem  37947  mapdordlem1a  38252  hdmapoc  38549  prjspeclsp  38707  rmydioph  39045  pw2f1ocnv  39068  rfovcnvf1od  39751  ntrneineine0lem  39834  funbrafv2b  42798  dfafn5a  42799  prprelb  43080