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  9068  eluz  12875  elicc4  13439  s111  14652  limsupgle  15527  lo1resb  15614  o1resb  15616  isercolllem2  15716  divalgmodcl  16464  ismri2  17687  acsfiel2  17710  eqglact  19246  eqgid  19247  cntzel  19392  dprdsubg  20095  subgdmdprd  20105  dprd2da  20113  dmdprdpr  20120  issubrg3  20684  ishil2  21837  obslbs  21848  iscld2  23153  isperf3  23278  cncnp2  23406  cnnei  23407  trfbas2  23968  flimrest  24108  flfnei  24116  fclsrest  24149  tsmssubm  24268  isnghm2  24849  isnghm3  24850  isnmhm2  24877  iscfil2  25393  caucfil  25410  ellimc2  26004  cnlimc  26015  lhop1  26141  dvfsumlem1  26153  fsumharmonic  27141  fsumvma  27342  fsumvma2  27343  vmasum  27345  chpchtsum  27348  chpub  27349  rpvmasum2  27641  dchrisum0lem1  27645  dirith  27658  uvtx2vtx1edg  29688  uvtx2vtx1edgb  29689  iscplgrnb  29706  frgr3v  30566  adjeu  32181  suppiniseg  32971  suppss3  33008  nndiffz1  33071  indpreima  33125  islinds5  33624  fsumcvg4  34284  qqhval2lem  34315  eulerpartlemf  34704  elorvc  34794  hashreprin  34951  neibastop3  36761  relowlpssretop  37897  sstotbnd2  38312  isbnd3b  38323  lshpkr  39780  isat2  39950  islln4  40170  islpln4  40194  islvol4  40237  islhp2  40660  pw2f1o2val2  43658  modelaxreplem3  45580  rfcnpre1  45630  rfcnpre2  45642  joindm3  49631  meetdm3  49633  catprsc  49675