Theorem baibd 539

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 528	. . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
3	2	bicomd 223	. 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃))
4	1, 3	sylan9bb 509	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:  rbaibd  540  bian1d  580  pw2f1olem  9021  eluz  12804  elicc4  13368  s111  14580  limsupgle  15441  lo1resb  15528  o1resb  15530  isercolllem2  15630  divalgmodcl  16378  ismri2  17600  acsfiel2  17623  eqglact  19156  eqgid  19157  cntzel  19300  dprdsubg  20003  subgdmdprd  20013  dprd2da  20021  dmdprdpr  20028  issubrg3  20579  ishil2  21701  obslbs  21712  iscld2  22995  isperf3  23120  cncnp2  23248  cnnei  23249  trfbas2  23810  flimrest  23950  flfnei  23958  fclsrest  23991  tsmssubm  24110  isnghm2  24691  isnghm3  24692  isnmhm2  24719  iscfil2  25235  caucfil  25252  ellimc2  25846  cnlimc  25857  lhop1  25983  dvfsumlem1  25995  fsumharmonic  26977  fsumvma  27178  fsumvma2  27179  vmasum  27181  chpchtsum  27184  chpub  27185  rpvmasum2  27477  dchrisum0lem1  27481  dirith  27494  uvtx2vtx1edg  29469  uvtx2vtx1edgb  29470  iscplgrnb  29487  frgr3v  30347  adjeu  31962  suppiniseg  32761  suppss3  32798  nndiffz1  32861  indpreima  32927  islinds5  33429  fsumcvg4  34096  qqhval2lem  34127  eulerpartlemf  34516  elorvc  34606  hashreprin  34766  neibastop3  36546  relowlpssretop  37682  sstotbnd2  38097  isbnd3b  38108  lshpkr  39565  isat2  39735  islln4  39955  islpln4  39979  islvol4  40022  islhp2  40445  pw2f1o2val2  43470  modelaxreplem3  45409  rfcnpre1  45452  rfcnpre2  45464  joindm3  49446  meetdm3  49448  catprsc  49490