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  3628  preddowncl  6335  ssimaex  6968  onfununi  8329  oaordex  8544  domtriord  9112  findcard3  9244  unfilem1  9266  inf0  9591  inf3lem3  9600  tcel  9713  fidomtri2  9981  alephval3  10095  zorn2lem6  10486  fodomb  10511  eqreznegel  12959  iserodd  16896  cshwsiun  17160  txcn  23764  ssfg  24010  fclsnei  24157  eldmgm  27167  fnrelpredd  35463  cvmlift2lem10  35785  axtco1from2  36967  bj-axreprepsep  37693  relcnveq3  38957  iss2  38974  elrelscnveq3  39257  jca3  39611  prjspreln0  43324  omabs2  44042  tfsconcatrn  44052  rfovcnvf1od  44713  mnuop3d  44964  ssclaxsep  45674