Theorem baibd 548

Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)

Hypothesis

Ref	Expression
baibd.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
baibd	⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

Proof of Theorem baibd

Step	Hyp	Ref	Expression
1		baibd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2		ibar 537	. . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
3	2	bicomd 226	. 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃))
4	1, 3	sylan9bb 518	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  rbaibd  549  bian1d  590  pw2f1olem  9065  eluz  12871  elicc4  13435  s111  14649  limsupgle  15524  lo1resb  15611  o1resb  15613  isercolllem2  15713  divalgmodcl  16460  ismri2  17683  acsfiel2  17706  eqglact  19242  eqgid  19243  cntzel  19388  dprdsubg  20091  subgdmdprd  20101  dprd2da  20109  dmdprdpr  20116  issubrg3  20699  ishil2  21869  obslbs  21880  iscld2  23185  isperf3  23310  cncnp2  23438  cnnei  23439  trfbas2  24000  flimrest  24140  flfnei  24148  fclsrest  24181  tsmssubm  24300  isnghm2  24881  isnghm3  24882  isnmhm2  24909  iscfil2  25425  caucfil  25442  ellimc2  26036  cnlimc  26047  lhop1  26173  dvfsumlem1  26185  fsumharmonic  27176  fsumvma  27377  fsumvma2  27378  vmasum  27380  chpchtsum  27383  chpub  27384  rpvmasum2  27676  dchrisum0lem1  27680  dirith  27693  uvtx2vtx1edg  29748  uvtx2vtx1edgb  29749  iscplgrnb  29766  frgr3v  30626  adjeu  32241  suppiniseg  33031  suppss3  33068  nndiffz1  33131  indpreima  33185  islinds5  33682  fsumcvg4  34340  qqhval2lem  34371  eulerpartlemf  34760  elorvc  34850  hashreprin  35007  neibastop3  36873  relowlpssretop  38010  sstotbnd2  38425  isbnd3b  38436  lshpkr  39891  isat2  40061  islln4  40281  islpln4  40305  islvol4  40348  islhp2  40771  pw2f1o2val2  43767  modelaxreplem3  45689  rfcnpre1  45739  rfcnpre2  45751  joindm3  49747  meetdm3  49749  catprsc  49791