Theorem mpan9 281

Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpan9.1	⊢ (𝜑 → 𝜓)
mpan9.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
mpan9	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mpan9.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5 32	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 125	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is referenced by:  sylan  283  vtocl2gf  2826  vtocl3gf  2827  vtoclegft  2836  sbcthdv  3004  disji2  4027  exmid1stab  4242  swopolem  4341  funssres  5301  fvmptssdm  5649  fmptcof  5732  fliftfuns  5848  isorel  5858  oveqrspc2v  5952  caovclg  6080  caovcomg  6083  caovassg  6086  caovcang  6089  caovordig  6093  caovordg  6095  caovdig  6102  caovdirg  6105  qliftfuns  6687  nneneq  6927  supmoti  7068  exmidonfinlem  7272  recexprlemopl  7709  recexprlemopu  7711  cauappcvgprlemladdrl  7741  caucvgsrlemcl  7873  caucvgsrlemfv  7875  caucvgsr  7886  suplocsrlempr  7891  ltordlem  8526  lble  8991  uz11  9641  seq3caopr3  10600  climcaucn  11533  sumdc  11540  fsum3  11569  fsumf1o  11572  fsum3cvg2  11576  isummulc2  11608  fsum2dlemstep  11616  fisumcom2  11620  fsumshftm  11627  fisum0diag2  11629  fsum00  11644  isumshft  11672  clim2prod  11721  prodmodclem2  11759  zproddc  11761  fprodseq  11765  fprodf1o  11770  prodssdc  11771  fprodm1s  11783  fprodp1s  11784  fprodcllemf  11795  fprodabs  11798  fprod2dlemstep  11804  fprodcom2fi  11808  dvdsprm  12330  pythagtriplem4  12462  pcmptdvds  12539  lidrididd  13084  grpidinv2  13260  ghmlin  13454  srgrz  13616  srglz  13617  ringinvnz1ne0  13681  rrgeq0i  13896  lmodlema  13924  islmodd  13925  lsslss  14013  ssnei2  14477  psmet0  14647  psmettri2  14648  cncfi  14898  dvcn  15020  dvmptfsum  15045  nninfsellemdc  15741