Theorem jca2 523

Description: Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)

Hypotheses

Ref	Expression
jca2.1	⊢ (𝜑 → (𝜓 → 𝜒))
jca2.2	⊢ (𝜓 → 𝜃)

Assertion

Ref	Expression
jca2	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Proof of Theorem jca2

Step	Hyp	Ref	Expression
1		jca2.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jca2.2	. . 3 ⊢ (𝜓 → 𝜃)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	1, 3	jcad 522	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ 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:  rr19.28v  3622  preddowncl  6330  ssimaex  6963  onfununi  8330  oaordex  8545  domtriord  9121  findcard3  9253  unfilem1  9275  inf0  9600  inf3lem3  9609  tcel  9722  fidomtri2  9999  alephval3  10113  zorn2lem6  10503  fodomb  10529  eqreznegel  12983  iserodd  16927  cshwsiun  17191  txcn  23852  ssfg  24098  fclsnei  24245  eldmgm  27258  fnrelpredd  35596  cvmlift2lem10  35891  axtco1from2  37094  bj-axreprepsep  37820  relcnveq3  39075  iss2  39092  elrelscnveq3  39375  jca3  39729  prjspreln0  43455  omabs2  44173  tfsconcatrn  44183  rfovcnvf1od  44844  mnuop3d  45095  ssclaxsep  45805