Theorem pm4.71rd 562

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	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	pm4.71d 561	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
3	2	biancomd 463	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  reueubd  3396  2reu5  3766  ralss  4069  rexss  4070  eqrrabd  4095  rabsneq  4648  reuhypd  5424  exopxfr2  5857  dfco2a  6267  onunel  6490  feu  6784  fcnvres  6785  funbrfv2b  6965  dffn5  6966  feqmptdf  6978  fimarab  6982  eqfnfv2  7051  dff4  7120  fmptco  7148  dff13  7274  opiota  8082  mpoxopovel  8243  brtpos  8258  dftpos3  8267  erinxp  8829  qliftfun  8840  pw2f1olem  9114  infm3  12224  prime  12696  predfz  13689  hashf1lem2  14491  hashle2prv  14513  oddnn02np1  16381  oddge22np1  16382  evennn02n  16383  evennn2n  16384  smueqlem  16523  vdwmc2  17012  acsfiel  17698  subsubc  17903  ismgmid  18690  eqger  19208  eqgid  19210  ghmqusker  19317  gaorber  19338  symgfix2  19448  znleval  21590  psrbaglefi  21963  bastop2  23016  elcls2  23097  maxlp  23170  restopn2  23200  restdis  23201  1stccn  23486  tx1cn  23632  tx2cn  23633  imasnopn  23713  imasncld  23714  imasncls  23715  idqtop  23729  tgqtop  23735  filuni  23908  uffix2  23947  cnflf  24025  isfcls  24032  fclsopn  24037  cnfcf  24065  ptcmplem2  24076  xmeter  24458  imasf1oxms  24517  prdsbl  24519  caucfil  25330  cfilucfil4  25368  shft2rab  25556  sca2rab  25560  mbfinf  25713  i1f1lem  25737  i1fres  25754  itg1climres  25763  mbfi1fseqlem4  25767  iblpos  25842  itgposval  25845  cnplimc  25936  ply1remlem  26218  plyremlem  26360  dvdsflsumcom  27245  fsumvma2  27272  vmasum  27274  logfac2  27275  chpchtsum  27277  logfaclbnd  27280  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  dchrisum0lem1  27574  colinearalg  28939  nbusgreledg  29384  nbusgredgeu0  29399  umgr2v2enb1  29558  iswwlksnx  29869  wspniunwspnon  29952  clwlknf1oclwwlknlem2  30110  clwlknf1oclwwlkn  30112  eupth2lem2  30247  eupth2lems  30266  frgrncvvdeqlem2  30328  fusgr2wsp2nb  30362  fusgreg2wsp  30364  pjpreeq  31426  elnlfn  31956  nfpconfp  32648  fmptcof2  32673  dfcnv2  32692  2ndpreima  32722  f1od2  32738  fpwrelmap  32750  iocinioc2  32787  nndiffz1  32794  algextdeglem6  33727  indpi1  34000  1stmbfm  34241  2ndmbfm  34242  eulerpartlemgh  34359  bnj1171  34992  mrsubrn  35497  elfuns  35896  fneval  36334  bj-imdirval3  37166  topdifinfindis  37328  uncf  37585  phpreu  37590  poimirlem23  37629  poimirlem26  37632  poimirlem27  37633  areacirclem5  37698  erimeq2  38659  prter3  38863  islshpat  38998  lfl1dim  39102  glbconxN  39360  cdlemefrs29bpre0  40378  dib1dim  41147  dib1dim2  41150  diclspsn  41176  dihopelvalcpre  41230  dih1dimatlem  41311  mapdordlem1a  41616  hdmapoc  41913  prjspeclsp  42598  rmydioph  43002  pw2f1ocnv  43025  onsupeqnmax  43235  orddif0suc  43257  cantnf2  43314  tfsconcat0i  43334  rfovcnvf1od  43993  ntrneineine0lem  44072  modelaxreplem3  44944  funbrafv2b  47108  dfafn5a  47109  prprelb  47440  stgredgiun  47860  gpgedgel  47942