Theorem jca2 513

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  rr19.28v  3637  preddowncl  6308  ssimaex  6949  onfununi  8313  oaordex  8525  domtriord  9093  findcard3  9236  findcard3OLD  9237  unfilem1  9261  fodomfibOLD  9289  inf0  9581  inf3lem3  9590  tcel  9705  fidomtri2  9954  alephval3  10070  zorn2lem6  10461  fodomb  10486  eqreznegel  12900  iserodd  16813  cshwsiun  17077  txcn  23520  ssfg  23766  fclsnei  23913  eldmgm  26939  fnrelpredd  35086  cvmlift2lem10  35306  relcnveq3  38316  iss2  38333  elrelscnveq3  38489  jca3  38856  prjspreln0  42604  omabs2  43328  tfsconcatrn  43338  rfovcnvf1od  44000  mnuop3d  44267  ssclaxsep  44979