Theorem jca2 522

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 521	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  rr19.28v  3630  preddowncl  6322  ssimaex  6956  onfununi  8316  oaordex  8531  domtriord  9099  findcard3  9231  unfilem1  9253  inf0  9578  inf3lem3  9587  tcel  9700  fidomtri2  9968  alephval3  10082  zorn2lem6  10473  fodomb  10498  eqreznegel  12946  iserodd  16883  cshwsiun  17147  txcn  23740  ssfg  23986  fclsnei  24133  eldmgm  27140  fnrelpredd  35392  cvmlift2lem10  35670  axtco1from2  36843  bj-axreprepsep  37567  relcnveq3  38833  iss2  38850  elrelscnveq3  39133  jca3  39487  prjspreln0  43198  omabs2  43916  tfsconcatrn  43926  rfovcnvf1od  44587  mnuop3d  44840  ssclaxsep  45550