Theorem jca2 517

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  rr19.28v  3608  preddowncl  6143  ssimaex  6723  onfununi  7961  oaordex  8167  domtriord  8647  findcard3  8745  unfilem1  8766  fodomfib  8782  inf0  9068  inf3lem3  9077  tcel  9171  fidomtri2  9407  alephval3  9521  zorn2lem6  9912  fodomb  9937  eqreznegel  12322  iserodd  16162  cshwsiun  16425  txcn  22231  ssfg  22477  fclsnei  22624  eldmgm  25607  fnrelpredd  32472  cvmlift2lem10  32672  relcnveq3  35738  iss2  35761  elrelscnveq3  35891  jca3  36152  prjspreln0  39603  rfovcnvf1od  40705  mnuop3d  40979