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  3634  preddowncl  6305  ssimaex  6946  onfununi  8310  oaordex  8522  domtriord  9087  findcard3  9229  findcard3OLD  9230  unfilem1  9254  fodomfibOLD  9282  inf0  9574  inf3lem3  9583  tcel  9698  fidomtri2  9947  alephval3  10063  zorn2lem6  10454  fodomb  10479  eqreznegel  12893  iserodd  16806  cshwsiun  17070  txcn  23513  ssfg  23759  fclsnei  23906  eldmgm  26932  fnrelpredd  35079  cvmlift2lem10  35299  relcnveq3  38309  iss2  38326  elrelscnveq3  38482  jca3  38849  prjspreln0  42597  omabs2  43321  tfsconcatrn  43331  rfovcnvf1od  43993  mnuop3d  44260  ssclaxsep  44972