Theorem baibd 549

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 538	. . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
3	2	bicomd 226	. 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃))
4	1, 3	sylan9bb 519	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  rbaibd  550  bian1d  591  pw2f1olem  9100  eluz  12979  elicc4  13544  s111  14763  limsupgle  15644  lo1resb  15731  o1resb  15733  isercolllem2  15833  divalgmodcl  16577  ismri2  17806  acsfiel2  17829  eqglact  19391  eqgid  19392  cntzel  19537  dprdsubg  20240  subgdmdprd  20250  dprd2da  20258  dmdprdpr  20265  issubrg3  20852  ishil2  22025  obslbs  22036  iscld2  23346  isperf3  23471  cncnp2  23599  cnnei  23600  trfbas2  24162  flimrest  24302  flfnei  24310  fclsrest  24343  tsmssubm  24462  isnghm2  25043  isnghm3  25044  isnmhm2  25071  iscfil2  25587  caucfil  25604  ellimc2  26197  cnlimc  26208  lhop1  26334  dvfsumlem1  26346  fsumharmonic  27339  fsumvma  27540  fsumvma2  27541  vmasum  27543  chpchtsum  27546  chpub  27547  rpvmasum2  27839  dchrisum0lem1  27843  dirith  27856  uvtx2vtx1edg  29979  uvtx2vtx1edgb  29980  iscplgrnb  29997  frgr3v  30876  adjeu  32491  suppiniseg  33279  suppss3  33315  nndiffz1  33378  indpreima  33432  islinds5  33923  fsumcvg4  34582  qqhval2lem  34613  eulerpartlemf  35002  elorvc  35092  hashreprin  35249  neibastop3  37150  relowlpssretop  38287  sstotbnd2  38708  isbnd3b  38719  lshpkr  40174  isat2  40344  islln4  40564  islpln4  40588  islvol4  40631  islhp2  41054  pw2f1o2val2  44046  modelaxreplem3  45969  rfcnpre1  46035  rfcnpre2  46047  joindm3  50076  meetdm3  50078  catprsc  50120