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  3622  preddowncl  6290  ssimaex  6919  onfununi  8273  oaordex  8485  domtriord  9051  findcard3  9183  unfilem1  9205  fodomfibOLD  9231  inf0  9530  inf3lem3  9539  tcel  9652  fidomtri2  9906  alephval3  10020  zorn2lem6  10411  fodomb  10436  eqreznegel  12847  iserodd  16763  cshwsiun  17027  txcn  23570  ssfg  23816  fclsnei  23963  eldmgm  26988  fnrelpredd  35247  cvmlift2lem10  35506  relcnveq3  38520  iss2  38537  elrelscnveq3  38800  jca3  39116  prjspreln0  42852  omabs2  43574  tfsconcatrn  43584  rfovcnvf1od  44245  mnuop3d  44512  ssclaxsep  45223