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  3610  preddowncl  6296  ssimaex  6925  onfununi  8281  oaordex  8493  domtriord  9061  findcard3  9193  unfilem1  9215  fodomfibOLD  9241  inf0  9542  inf3lem3  9551  tcel  9664  fidomtri2  9918  alephval3  10032  zorn2lem6  10423  fodomb  10448  eqreznegel  12884  iserodd  16806  cshwsiun  17070  txcn  23591  ssfg  23837  fclsnei  23984  eldmgm  26985  fnrelpredd  35234  cvmlift2lem10  35494  axtco1from2  36657  bj-axreprepsep  37382  relcnveq3  38648  iss2  38665  elrelscnveq3  38948  jca3  39302  prjspreln0  43042  omabs2  43760  tfsconcatrn  43770  rfovcnvf1od  44431  mnuop3d  44698  ssclaxsep  45409