Theorem impel 511

Description: An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)

Hypotheses

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

Assertion

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

Proof of Theorem impel

Step	Hyp	Ref	Expression
1		impel.2	. . 3 ⊢ (𝜃 → 𝜓)
2		impel.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	imp 408	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  equs5e  2468  mob2  3658  ssn0rex  4289  reusv2lem2  5331  copsex2t  5436  reuop  6248  trssord  6331  trsuc  6403  funimass2  6572  fvelima  6896  fvmptf  6961  funfvima2  7179  funfvima3  7184  tfi  7797  suppssov1  8141  suppssov2  8142  tposf2  8194  frrlem4  8233  ectocld  8723  mapsnd  8828  resixpfo  8878  f1oeng  8911  nneneq  9134  fodomfi  9216  fiint  9231  fodomfiOLD  9234  eqinf  9392  hartogslem1  9451  cantnf  9609  rankwflemb  9712  carden2a  9885  carduni  9900  harval2  9916  cardaleph  10006  alephval3  10027  dfac5  10046  cfcof  10191  axdc4lem  10372  nqereu  10847  recexsr  11025  seqcoll  14421  swrdswrd  14662  swrdccatin1  14682  swrdccatin2  14686  repswswrd  14741  climcau  15628  odd2np1  16305  lcmfunsnlem2lem2  16603  coprmproddvdslem  16626  dvdsprm  16668  vdwlem6  16952  imasvscafn  17496  dirref  18562  irredn1  20401  isdrngd  20741  isdrngdOLD  20743  psgnghm  21559  gsummoncoe1  22298  prdstopn  23615  cnextcn  24054  tnggrpr  24642  ovolctb  25479  dyadmbl  25589  itg1addlem4  25688  itg1le  25702  dvcnp2  25909  c1liplem1  25985  pserulm  26409  fsumdvdsmul  27180  perfectlem2  27215  dchrisumlem2  27475  noresle  27683  bday1  27828  readdscl  28513  remulscl  28516  axlowdimlem16  29048  wlkv0  29740  wlkp1lem1  29762  wlkswwlksf1o  29969  wspniunwspnon  30013  trlsegvdeglem1  30312  frcond4  30362  2clwwlk2clwwlk  30442  opabssi  32709  nn0xmulclb  32867  zarclsiin  34067  rankval4b  35296  cusgr3cyclex  35379  satfun  35654  fundmpss  36010  nn0prpw  36566  bj-restpw  37465  bj-prmoore  37488  cgsex2gd  37512  domalom  37781  cover2  38097  disjlem18  39285  sticksstones11  42656  setindtr  43484  onov0suclim  43734  oe0suclim  43737  ofoaid1  43818  ofoaid2  43819  naddcnfcom  43826  naddcnfass  43829  omssaxinf2  45447  climxlim2lem  46302  sge0f1o  46839  2reuimp  47592  fvelsetpreimafv  47876  imasetpreimafvbijlemfo  47894  reupr  48011  lighneallem4  48102  proththd  48106  lincresunit3  48986  oppc1stflem  49791