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  3623  preddowncl  6280  ssimaex  6908  onfununi  8264  oaordex  8476  domtriord  9040  findcard3  9172  unfilem1  9194  fodomfibOLD  9221  inf0  9517  inf3lem3  9526  tcel  9641  fidomtri2  9890  alephval3  10004  zorn2lem6  10395  fodomb  10420  eqreznegel  12835  iserodd  16747  cshwsiun  17011  txcn  23511  ssfg  23757  fclsnei  23904  eldmgm  26930  fnrelpredd  35062  cvmlift2lem10  35295  relcnveq3  38305  iss2  38322  elrelscnveq3  38478  jca3  38845  prjspreln0  42592  omabs2  43315  tfsconcatrn  43325  rfovcnvf1od  43987  mnuop3d  44254  ssclaxsep  44966