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  9082  eluz  12904  elicc4  13469  s111  14686  limsupgle  15567  lo1resb  15654  o1resb  15656  isercolllem2  15756  divalgmodcl  16500  ismri2  17723  acsfiel2  17746  eqglact  19307  eqgid  19308  cntzel  19453  dprdsubg  20156  subgdmdprd  20166  dprd2da  20174  dmdprdpr  20181  issubrg3  20765  ishil2  21935  obslbs  21946  iscld2  23256  isperf3  23381  cncnp2  23509  cnnei  23510  trfbas2  24072  flimrest  24212  flfnei  24220  fclsrest  24253  tsmssubm  24372  isnghm2  24953  isnghm3  24954  isnmhm2  24981  iscfil2  25497  caucfil  25514  ellimc2  26107  cnlimc  26118  lhop1  26244  dvfsumlem1  26256  fsumharmonic  27251  fsumvma  27452  fsumvma2  27453  vmasum  27455  chpchtsum  27458  chpub  27459  rpvmasum2  27751  dchrisum0lem1  27755  dirith  27768  uvtx2vtx1edg  29861  uvtx2vtx1edgb  29862  iscplgrnb  29879  frgr3v  30758  adjeu  32373  suppiniseg  33161  suppss3  33197  nndiffz1  33260  indpreima  33314  islinds5  33805  fsumcvg4  34463  qqhval2lem  34494  eulerpartlemf  34884  elorvc  34974  hashreprin  35131  neibastop3  36984  relowlpssretop  38121  sstotbnd2  38527  isbnd3b  38538  lshpkr  39993  isat2  40163  islln4  40383  islpln4  40407  islvol4  40450  islhp2  40873  pw2f1o2val2  43884  modelaxreplem3  45806  rfcnpre1  45856  rfcnpre2  45868  joindm3  49898  meetdm3  49900  catprsc  49942