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  3636  preddowncl  6330  ssimaex  6964  onfununi  8324  oaordex  8539  domtriord  9107  findcard3  9239  unfilem1  9261  inf0  9586  inf3lem3  9595  tcel  9708  fidomtri2  9976  alephval3  10090  zorn2lem6  10481  fodomb  10506  eqreznegel  12954  iserodd  16891  cshwsiun  17155  txcn  23748  ssfg  23994  fclsnei  24141  eldmgm  27148  fnrelpredd  35421  cvmlift2lem10  35699  axtco1from2  36871  bj-axreprepsep  37595  relcnveq3  38861  iss2  38878  elrelscnveq3  39161  jca3  39515  prjspreln0  43226  omabs2  43944  tfsconcatrn  43954  rfovcnvf1od  44615  mnuop3d  44866  ssclaxsep  45576