Theorem ifboth 4565

Description: A wff 𝜃 containing a conditional operator is true when both of its cases are true. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 15-Feb-2015.)

Hypotheses

Ref	Expression
ifboth.1	⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
ifboth.2	⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
ifboth	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem ifboth

Step	Hyp	Ref	Expression
1		ifboth.1	. 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
2		ifboth.2	. 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
3		simpll 767	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜓)
4		simplr 769	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ ¬ 𝜑) → 𝜒)
5	1, 2, 3, 4	ifbothda 4564	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  ifcl  4571  keephyp  4597  soltmin  6156  xrmaxlt  13223  xrltmin  13224  xrmaxle  13225  xrlemin  13226  ifle  13239  expmulnbnd  14274  limsupgre  15517  isumless  15881  cvgrat  15919  rpnnen2lem4  16253  ruclem2  16268  sadcaddlem  16494  sadadd3  16498  pcmptdvds  16932  prmreclem5  16958  prmreclem6  16959  pnfnei  23228  mnfnei  23229  xkopt  23663  xmetrtri2  24366  stdbdxmet  24528  stdbdmet  24529  stdbdmopn  24531  xrsxmet  24831  icccmplem2  24845  metdscn  24878  metnrmlem1a  24880  ivthlem2  25487  ovolicc2lem5  25556  ioombl1lem1  25593  ioombl1lem4  25596  ismbfd  25674  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  itg2const  25775  itg2const2  25776  itg2monolem3  25787  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  iblss  25840  itgless  25852  ibladdlem  25855  iblabsr  25865  iblmulc2  25866  bddiblnc  25877  dvferm1lem  26022  dvferm2lem  26024  dvlip2  26034  dgradd2  26308  plydiveu  26340  chtppilim  27519  dchrvmasumiflem1  27545  ostth3  27682  1smat1  33803  poimirlem24  37651  mblfinlem2  37665  itg2addnclem  37678  itg2addnc  37681  itg2gt0cn  37682  ibladdnclem  37683  iblmulc2nc  37692  ftc1anclem5  37704  ftc1anclem8  37707  ftc1anc  37708